Global Variables and Constants

CLAIRE offers the possibility to define global variables; they are named objects from the following class :

global_variable <: thing(range:type, value:any)

For instance, one can create the following :

tata :: global_variable(range = integer,                          value = 12)

However, there is a shorthand notation :

tata:integer :: 12

Notice that, contrary to languages such as C++, you always must provide an initialization value when you define a global variable (it may be the unknown value). Variables can be used anywhere, following the visibility rules of their identifiers. Their value can be changed directly with the same syntax as local variables.

tata := 12, tata :+ 1, tata :- 10

The value that is assigned to a global variable must always belong to its range, with the exception of the unknown value, which is allowed. If a variable is re-defined, the new value replaces the old one, with the exception still of unknown, which does not replace the previous value. This is useful for defining flags, which are global_variables that are set from the outside (e.g., by the compiler). One could write, for instance,

talk:boolean :: unknown  (#if talk printf(...))

The value of talk may be set to false before running the program to avoid loading the printf statements. When the value does not change, it is simpler to just assign a value to an identifier. For instance :

toto :: 13

binds the value 13 to the identifier toto. This is useful to define aliases, especially when we use imported objects from other modules. For instance, if we use Logic/Algebra/exp, we may want to define a simpler alias with :

exp :: Logic/Algebra/exp

The value assigned to a global variable may be made part of a world definition and thus restored by backtracking using choice/backtrack. It is simply required to declare the variable as a defeasible (i.e., backtrack -able) variable using the store declaration as for a relation :

store(tata)  (tata := 1, choice(), tata := 2, backtrack(), assert(tata = 1))